(**************************************************************************)
(*                                                                        *)
(*                                  Cubicle                               *)
(*             Combining model checking algorithms and SMT solvers        *)
(*                                                                        *)
(*                  Sylvain Conchon and Alain Mebsout                     *)
(*                  Universite Paris-Sud 11                               *)
(*                                                                        *)
(*  Copyright 2011. This file is distributed under the terms of the       *)
(*  Apache Software License version 2.0                                   *)
(*                                                                        *)
(**************************************************************************)

exception ReachBound

type op_comp = Eq | Lt | Le | Neq
type op_arith = Plus | Minus

type sort = Glob | Arr | Constr | Var

type const = ConstInt of Num.num | ConstReal of Num.num | ConstName of string

type term = 
  | Const of const
  | Elem of string * sort
  | Access of string * string list
  | Arith of term * const

(* val compare_term : term -> term -> int *)

type acc_eq = { a : string; i: string; e: term }

module rec Atom : sig
  type t =
    | True
    | False
    | Comp of term * op_comp * term
    | Ite of SAtom.t * t * t

  val compare : t -> t -> int
end 
and SAtom : Set.S with type elt = Atom.t

type update = {
  up_arr : string;
  up_arg : string list;
  up_swts : (SAtom.t * term) list;
}

(* DAVID : Plus utilisé *)
(*type action = Aassign of string * term | Aupd of update | Anondet of string*)
    
type transition = {
  tr_name : string;
  tr_args : string list;
  tr_reqs : SAtom.t;
  tr_ureq : (string * SAtom.t list) list;
  tr_assigns : (string * term) list;
  tr_upds : update list;
  tr_nondets : string list
}

type elem = string * (string list)

type decl = Dglobal of string * string | Dconst of string * string
            | Darray of string * (string list * string)



type decls =
    | Dlist of decl list
    | Dapp of decls * decls

val nop : decls

val decl_l: decl list -> decls

val (++) : decls -> decls -> decls

                
type system = {
  type_defs : elem list;
  decls : decls;
  init : string option * SAtom.t;
  invs : (string list * SAtom.t) list;
  cands : (string list);
  unsafe : (string list * SAtom.t) list;
  forward : (string list * string list * SAtom.t) list;
  trans : transition list
}

(* Pretty-printer *)


  
val print_system : Format.formatter -> system -> unit

val print_op_comp : Format.formatter -> op_comp -> unit
val print_const : Format.formatter -> const -> unit
val print_term : Format.formatter -> term -> unit
val print_atom : Format.formatter -> Atom.t -> unit
val print_satom : Format.formatter -> SAtom.t -> unit
val print_transition : Format.formatter -> transition -> unit
val print_unsafe : Format.formatter -> (string list * SAtom.t) -> unit
val print_invs : Format.formatter -> (string list * SAtom.t) list -> unit
val print_init : Format.formatter -> (string option * SAtom.t) -> unit
val print_typedef: Format.formatter -> elem list -> unit
val print_decl : Format.formatter -> decl -> unit
val print_decls : Format.formatter -> decls -> unit
  


  














